Termination Proof Script

• Consider the SCC {11,15}. There are no usable rules. By taking the AF π with π(ACTIVATE) = 1, π(FIRST) = π(n__first) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 15 is weakly decreasing and rule 11 is strictly decreasing.


• Consider the SCC {12}. The usable rules are {1-3,6-10}. By taking the AF π with π(first) = π(n__first) = π(SEL) = 1, π(cons) = 2 and π(from) = π(n__from) = [ ] together with the lexicographic path order with precedence 0 ≻ nil and activate ≻ from ≻ n__from, rule 7 is weakly decreasing and the rules in {1-3,6,8-10,12} are strictly decreasing.